This paper presents SYMRT, a tool based on a combination of symbolic execution and real-time model checking for\ntiming analysis of Java systems. Symbolic execution is used for the generation of a safe and tight timing model of the\nanalyzed system capturing the feasible execution paths. The model is combined with suitable execution environment\nmodels capturing the timing behavior of the target host platform including the Java virtual machine and complex\nhardware features such as caching. The complete timing model is a network of timed automata which directly\nfacilitates safe estimates of worst and best case execution time to be determined using the UPPAAL model checker.\nFurthermore, the integration of the proposed techniques into the TETASARTS tool facilitates reasoning about additional\ntiming properties such as the schedulability of periodically and sporadically released Java real-time tasks (under specific\nscheduling policies), worst case response time, and more.
Loading....